\begin{tabbing} $\forall$${\it the\_w}$:World, $e$:E, $t$:$\mathbb{N}$. \\[0ex]FairFifo \\[0ex]$\Rightarrow$ ($\uparrow$isrcv(kind($e$))) \\[0ex]$\Rightarrow$ ($\uparrow$match(lnk(kind($e$));$t$;time($e$))) \\[0ex]$\Rightarrow$ (\=onlnk(lnk(kind($e$));m(source(lnk(kind($e$)));$t$))[($\parallel$rcvs(lnk(kind($e$));time($e$))$\parallel$ \+ \\[0ex]{-} $\parallel$snds(lnk(kind($e$));$t$)$\parallel$)] \\[0ex]= \\[0ex]msg(a(loc($e$);time($e$))) \\[0ex]$\in$ Msg) \- \end{tabbing}